perf(verifier): compute shared LogUp α-powers once, slice per table - #842
perf(verifier): compute shared LogUp α-powers once, slice per table#842diegokingston wants to merge 1 commit into
Conversation
step_2 rebuilt [1, α, α², …] (α-powers up to the table's bus width) once per table via compute_alpha_powers, even though the LogUp α challenge is a single value sampled once in multi_verify_views and shared across every table. Each table's power vector is just a prefix of the same geometric sequence. Compute the sequence ONCE after sampling the shared challenges — to the global-max bus width across all AIRs — and slice each table's prefix in step_2. Saves (Σ_tables max_bus_elements − max_bus_elements) ext-field multiplications and N−1 heap allocations per proof (allocations = proven memory-table writes in the recursion guest). Byte-identical: the sliced prefix equals what each table computed before. 204 stark tests pass, clippy clean, prover builds.
|
/bench-verify |
|
⏳ Benchmark started on the bench server. The verifier bench takes ~5 min; the recursion-guest cycle comparison then adds guest builds — a few minutes when cached, up to ~1h on a cold run. The bench server is occupied until it finishes. |
Verifier benchmark —
|
| Metric | main | PR | Δ |
|---|---|---|---|
| Verify time | 3.587s | 3.583s | -0.09% ⚪ |
| Proof size | 204.30 MiB | 204.30 MiB | +0.00% ⚪ |
pairs: 20 mean A (PR): 3.583s mean B (main): 3.587s
[parametric] paired-t mean -0.09% sd 0.80% se 0.18%
95% CI: [-0.47%, +0.28%] (t df=19 = 2.093)
[robust] median -0.10% Wilcoxon W+=49 W-=161 p(exact)=0.0362 (z=-2.07)
run-to-run jitter: A CV 0.66% B CV 0.47% (lower = steadier)
within-session drift: +0.13% over the run, 1st->2nd half +0.16%
⚪ BORDERLINE — parametric and robust disagree; suspect outlier pair(s). Trust the median (-0.10%); add pairs.
Drift-free interleaved A/B/B/A measurement. - = PR faster. Trust the verdict when paired-t and Wilcoxon agree.
Recursion guest cycles (main vs PR)
=== Recursion-guest cycle comparison — single query (blowup=2, 1 query) — deterministic to ~±100k cycles ===
REF_B (baseline) origin/main a864832 guest=recursion-min.elf
REF_A (PR) a4b3aaa a4b3aaa guest=recursion-min.elf
| Metric | REF_B (baseline) | REF_A (PR) | Δ (A-B) |
|---|---|---|---|
| Guest cycles | 43.6M | 38.2M | -5.4M (-12.44%) |
| Keccak calls | 3025 | 3025 | 0 |
note: cycles reproduce to ~±100k (build codegen + proof nondeterminism); treat sub-100k deltas as noise, not signal.
raw (exact integer counts)
ref_b_sha=a8648320867f7f4242fe286a5b266ffed1fb5519 ref_b_elf=recursion-min.elf ref_b_cycles=43608950 ref_b_keccak=3025 ref_b_execute_wall_s=1
ref_a_sha=a4b3aaacf09c154bf4a20995d599c537b2c83153 ref_a_elf=recursion-min.elf ref_a_cycles=38182244 ref_a_keccak=3025 ref_a_execute_wall_s=2
delta_cycles=-5426706 delta_keccak=0
There was a problem hiding this comment.
⚠️ AI-generated review. Produced by an automated agent and posted from this account — not written by hand. Findings below are leads to verify, not confirmed conclusions.
Hoists the α-power sequence into multi_verify_views and slices it per table, replacing the per-table compute_alpha_powers rebuilds of prefixes of one geometric sequence. The transform is equivalent: same α, same prefix, no absorb or squeeze moved, and the build-site guard (lookup_challenges.len() > LOGUP_CHALLENGE_ALPHA) and the slice-site guard (challenges.rap_challenges.len() > …) read the same vector because replay_rounds_after_round_1 stores rap_challenges unmodified. Two items before merge.
.github/scripts/run_recursion_bench.sh:18 (and .github/workflows/bench-verify.yml:111) — the posted −5.4M cycles (−12.44%) is not this change's win. Both benches hardcode origin/main as the baseline, but this PR is based on perf/verifier-amortize-tier01, so REF_B a8648320 is the merge-base and the delta also contains 4d4d8868 (shared zerofier + batched DEEP inversions) and 1ea78769 (reused trace root + shared Q FRI points) — both on per-query paths that run 110–219 times per proof, versus this change's once-per-table work. This commit's own saving is (Σ_tables max_bus_elements − max_t max_bus_elements) extension muls plus ~N−1 small allocations over ~31 tables: tens of thousands of guest cycles, under the script's own stated ±100k noise floor. The native −0.09% BORDERLINE matches that. Re-run against 1ea78769, or state in the body that the headline is stack-cumulative so it isn't credited again when #830 lands. The workflow should use the PR's base ref (or merge-base with it) rather than hardcoded origin/main, otherwise every stacked verifier PR inherits this.
crypto/stark/src/verifier.rs:306 — &shared_alpha_powers[..air.max_bus_elements()] is a panicking index on a verifier-executed path, justified by a comment about an invariant maintained two frames up. The invariant holds today (one call site for verify_rounds_2_to_4, one empty trait impl, both lengths derived from the same airs slice, max_bus_elements is AIR metadata and not proof-derived), so it is not attacker-reachable. But after the #833 revert the bar is no panic on a verifier path even for AIR-metadata invariants, since a panic in the recursion guest kills execution instead of yielding a rejectable proof. Keeping the property local costs nothing:
let logup_alpha_powers: &[FieldElement<FieldExtension>] =
shared_alpha_powers.get(..air.max_bus_elements()).unwrap_or(&[]);Behaviourally identical on every reachable state — when no challenges were sampled the shared vector is empty and get yields &[], exactly the old else arm — it deletes the branch and fails closed. match … { Some(p) => p, None => return false } inside the existing guard works equally well if rejecting loudly is preferred.
Nits:
- verifier.rs:302 — "when the proof carries LogUp challenges" implies the prover decides whether challenges exist; they are verifier-sampled and gated on
needs_lookup_challenges = airs.iter().any(|air| air.has_aux_trace()), pure AIR layout. Same phrasing in the PR body. - verifier.rs:1379 —
lookup_challenges.clone()sits directly above the new argument and is a 2-element Vec allocation per table, the same per-table alloc cost this PR removes; fixing it needs a lifetime onChallenges, but it caps the allocation win being claimed.
2 participants
Stacked on #830.
What
step_2_verify_claimed_composition_polynomialrebuilt the LogUp α-power vector[1, α, α², …](up to the table's bus width) once per table viacompute_alpha_powers, even though the LogUp α challenge is a single value sampled once inmulti_verify_views(Round 1 Phase B) and shared across every table. Each table's vector is just a prefix of the same geometric sequence.This computes the sequence once, right after sampling the shared challenges, to the global-max bus width across all AIRs, and each table's
step_2slices the prefix it needs.Why
The verifier doubles as the serial recursion guest, so per-table recompute costs real cycles:
(Σ_tables max_bus_elements − max_t max_bus_elements)extension-field multiplications per proof (E×E ≈ 9 base muls each).N−1heap allocations per proof — each heap alloc is a proven memory-table write in the guest.Correctness
Byte-identical: the sliced prefix
&shared_alpha_powers[..air.max_bus_elements()]equals the vector each table computed before. When the proof carries LogUp challenges,shared_alpha_powers.len()is the global max, so every table's slice is in range; otherwise both old and new paths yield an empty slice. Comment atlookup.rs:96documents that α must be shared across all AIRs.Testing